import encodings
import subprocess
import os

def generate_and_test_cnf(variables, clauses, index, base_path):
    # Generate CNF file using cnfgen
    cnf_file = f"{base_path}/temp-{index}.cnf"
    with open(cnf_file, "w") as file:
        subprocess.run(["cnfgen", "-o", cnf_file, "randkcnf", str(variables), str(clauses)], stdout=file)

    # Test CNF file using kissat
    result = subprocess.run(["kissat", "-q", cnf_file], capture_output=True, text=True)

    # Determine if the CNF is satisfiable or not
    if "s SATISFIABLE" in result.stdout:
        new_name = f"{base_path}/sat-20-{clauses}-{index}.cnf"
    else:
        new_name = f"{base_path}/uns-20-{clauses}-{index}.cnf"
    
    # Rename the file accordingly
    os.rename(cnf_file, new_name)

def main():
    variables = 20
    clauses = 91  # This may need adjustment based on empirical results
    base_path = "cnf/local"
    sat_count = uns_count = 0
    index = 0

    while sat_count < 500 or uns_count < 500:
        generate_and_test_cnf(variables, clauses, index, base_path)
        if "sat" in f"sat-20-{clauses}-{index}.cnf":
            sat_count += 1
        else:
            uns_count += 1
        index += 1
        print(f"Generated {sat_count} satisfiable and {uns_count} unsatisfiable so far")

if __name__ == "__main__":
    main()
